es:ES, l:IdLnk, tg:Id, B:Type, P:({e:E| loc(e) = source(l)  Id }Prop),
f:({e:E| loc(e) = source(l)  Id }B), ds:x:Id fp Type.
es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e))  Prop 

latex

Definitions	ES, t  T, IdLnk, Id, Prop, x:A. B(x), source(l), loc(e), E, x. t(x), a:A fp B(a), P & Q, A & B, {T}, P  Q, sender(e), 1of(t), kind(e), Knd, rcv(l,tg), x(s), valtype(e), val(e), x:A. B(x), e@i. P(e), Top, IdDeq, vartype(i;x), f(x)?z, es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e))
Lemmas	es-valtype wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, alle-at wf, es-val wf, rcv wf, Knd wf, es-kind wf, es-sender wf, es-kind-rcv, fpf wf, es-E wf, es-loc wf, lsrc wf, Id wf, IdLnk wf, event system wf